Nuprl Definition : loset
13,42
postcript
pdf
LOSet == {
s
:POSet{i}| Connex(|
s
|;
x
,
y
.
x
y
)}
latex
clarification:
LOSet{i} == {
s
:POSet{i}| Connex(|
s
|;
x
,
y
.
x
s
y
)}
latex
Up
sets
1
Wellformedness Lemmas
loset
wf
Definitions
POSet{i}
,
Connex(
T
;
x
,
y
.
R
(
x
;
y
))
,
|
p
|
,
a
b
origin
y)}
s y)} y)}
s y)} b